[Lucas - TR'03, Example 2]

Example 2 in [Lucas - TR'03]

Summary: Ex2_Luc03b

CS-TRS Ex2_Luc03b (file Ex2_Luc03b.csr)

Functions:  0 s nil cons fst from add len

Constructors:  0 s nil cons

Variables:  X Y Z

Arities: 

ar(0) = 0
ar(s) = 1
ar(nil) = 0
ar(cons) = 2
ar(fst) = 2
ar(from) = 1
ar(add) = 2
ar(len) = 1

Replacement map: 

µ(0)={}
µ(s)={}
µ(nil)={}
µ(cons)={1}
µ(fst)={1,2}
µ(from)={1}
µ(add)={1,2}
µ(len)={1}

Rules: (file Ex2_Luc03b) 

fst(0,Z) -> nil
fst(s(X),cons(Y,Z)) -> cons(Y,fst(X,Z))
from(X) -> cons(X,from(s(X)))
add(0,X) -> X
add(s(X),Y) -> s(add(X,Y))
len(nil) -> 0
len(cons(X,Z)) -> s(len(Z))

The CS-TRS in OBJ format (file Ex2_Luc03b.obj):

obj Ex2_Luc03b is
  sorts Nat LNat .
  op 0     : -> Nat .
  op s     : Nat -> Nat [strat (0)] .
  op nil   : -> LNat .
  op cons  : Nat LNat -> LNat [strat (1)] .
  op fst   : Nat LNat -> LNat .
  op from  : Nat -> LNat .
  op add   : Nat Nat -> Nat .
  op len   : LNat -> Nat .
  vars X Y : Nat .
  var Z    : LNat .
  eq fst(0,Z) = nil .
  eq fst(s(X),cons(Y,Z)) = cons(Y,fst(X,Z)) .
  eq from(X) = cons(X,from(s(X))) .
  eq add(0,X) = X .
  eq add(s(X),Y) = s(add(X,Y)) .
  eq len(nil) = 0 .
  eq len(cons(X,Z))= s(len(Z)) .
endo

Negative results

--

Positive results

  1. Ex2_Luc03b is proved µ-terminating in [Luc03b, Example 11] by using Lucas' transformation. The TRS Ex2_Luc03b_L: 
       fst(0,Z) -> nil
   fst(s,cons(Y)) -> cons(Y)
   from(X) -> cons(X)
   add(0,X) -> X
   add(s,Y) -> s
   len(nil) -> 0
   len(cons(X)) -> s
    is terminating (use MuTerm).
  2. The µ-termination of Ex2_Luc03b can also be proved by using Zantema's transformation. The TRS Ex2_Luc03b_Z: 
       fst(0,Z) -> nil
   fst(s(X),cons(Y,Z)) -> cons(Y,n__fst(activate(X),activate(Z)))
   from(X) -> cons(X,n__from(s(X)))
   add(0,X) -> X
   add(s(X),Y) -> s(n__add(activate(X),Y))
   len(nil) -> 0
   len(cons(X,Z)) -> s(n__len(activate(Z)))
   fst(X1,X2) -> n__fst(X1,X2)
   from(X) -> n__from(X)
   add(X1,X2) -> n__add(X1,X2)
   len(X) -> n__len(X)
   activate(n__fst(X1,X2)) -> fst(X1,X2)
   activate(n__from(X)) -> from(X)
   activate(n__add(X1,X2)) -> add(X1,X2)
   activate(n__len(X)) -> len(X)
   activate(X) -> X
    is terminating (use MuTerm).
  3. The µ-termination of Ex2_Luc03b can also be proved by using Ferreira and Ribeiro's transformation. The TRS Ex2_Luc03b_FR: 
       fst(0,Z) -> nil
   fst(s(X),cons(Y,Z)) -> cons(Y,n__fst(activate(X),activate(Z)))
   from(X) -> cons(X,n__from(n__s(X)))
   add(0,X) -> X
   add(s(X),Y) -> s(n__add(activate(X),Y))
   len(nil) -> 0
   len(cons(X,Z)) -> s(n__len(activate(Z)))
   fst(X1,X2) -> n__fst(X1,X2)
   from(X) -> n__from(X)
   s(X) -> n__s(X)
   add(X1,X2) -> n__add(X1,X2)
   len(X) -> n__len(X)
   activate(n__fst(X1,X2)) -> fst(activate(X1),activate(X2))
   activate(n__from(X)) -> from(activate(X))
   activate(n__s(X)) -> s(X)
   activate(n__add(X1,X2)) -> add(activate(X1),activate(X2))
   activate(n__len(X)) -> len(activate(X))
   activate(X) -> X
    is terminating (use MuTerm).
  4. The µ-termination of Ex2_Luc03b can also be proved by using Giesl and Middeldorp's transformation. The TRS Ex2_Luc03b_GM: 
       a__fst(0,Z) -> nil
   a__fst(s(X),cons(Y,Z)) -> cons(mark(Y),fst(X,Z))
   a__from(X) -> cons(mark(X),from(s(X)))
   a__add(0,X) -> mark(X)
   a__add(s(X),Y) -> s(add(X,Y))
   a__len(nil) -> 0
   a__len(cons(X,Z)) -> s(len(Z))
   mark(fst(X1,X2)) -> a__fst(mark(X1),mark(X2))
   mark(from(X)) -> a__from(mark(X))
   mark(add(X1,X2)) -> a__add(mark(X1),mark(X2))
   mark(len(X)) -> a__len(mark(X))
   mark(0) -> 0
   mark(s(X)) -> s(X)
   mark(nil) -> nil
   mark(cons(X1,X2)) -> cons(mark(X1),X2)
   a__fst(X1,X2) -> fst(X1,X2)
   a__from(X) -> from(X)
   a__add(X1,X2) -> add(X1,X2)
   a__len(X) -> len(X)
    is terminating (use MuTerm).
  5. The µ-termination of Ex2_Luc03b can also be proved by using a polynomial interpretation (computed with MuTerm): 
       [0] = 2
   [s](X) = 0
   [nil] = 1
   [cons](X1,X2) = X1 + 1
   [fst](X1,X2) = X1 + 2.X2
   [from](X) = X + 2
   [add](X1,X2) = X1 + X2 + 1
   [len](X) = 3.X
  6. The µ-termination of Ex2_Luc03b can be proved by using CSRPO (proof due to Albert Rubio). Automatically can be proved by MuTerm :
    • marking map: 
         m(cons,2)={from,fst}=W
   m(s,1)={len,add}=V
   m(fst',1)={len,add}=V
   m(add',1)={len,add}=V
   m(fst',2)={from,fst}=W
   m(len',1)={from,fst}=W
    • precedence: 
         fst > nil, cons, fst'
   from > cons, from', s
   add > s, add'
   len> 0, s,len'
    • status: 
             st(f) = mul for all function symbols
  7. The µ-termination of Ex2_Luc03b can be proved by using CSDP (computed by MuTerm).